// AbstractionTerm.cpp : implementation file
/*
#ifndef _ABSTRACTTERM_CPP
#define _ABSTRACTTERM_CPP

#ifdef _STDAFX_H
*/
#include "stdafx.h"
//#endif 

#include "AbstractTerm.h"

//#ifndef _APPLICATIONTERM_CPP
#include "ApplicationTerm.h"
//#endif

size_t AbstractTerm::complexity() const {
	return	getVar().complexity() + 
				getBody().complexity() + 
				Term::complexity();
	}

bool AbstractTerm::TypeOccursinFreeVariable(Type::const_reference Ty) const {
	return getBody().TypeOccursinFreeVariable(Ty);
	}

Term::pointer AbstractTerm::normalized() const{
	Term::pointer newBody =  getBody().normalized();
	Term::pointer Res = new AbstractTerm(*newBody, getVar(), this->getSyntax());
	delete newBody;
	return Res;
}
Token::pointer AbstractTerm::applyArgument(Token::const_reference Ter) const {
	if(Ter.isTerm())
		if(_TERM(Ter).getType() == getVar().getType())
			return getBody().replaceAll(getVar(), Ter);
		
	throw Term::exception("Unable to process Term at AbstractTerm::applyArgument");
}
Token::pointer AbstractTerm::clone() const{
		return new AbstractTerm(*this);
}
bool AbstractTerm::isReducible() const{
	return getBody().isReducible();
	}
string AbstractTerm::toString() const{
	if(this->SyntacticSugar.size()>0)
		return Token::toString();

	return string("(")+getVar().toString() + ") @ {"
		+getBody().toString() +string("}");
		}
string AbstractTerm::view () const{
		return	string("[")+getVar().view()+"@("
					+getBody().view()+
					")]:"
					+getType().view();
		}


bool AbstractTerm::operator==(Token::const_reference To) const{	
	if(To.isTerm())
		if((_TERM(To)).isAbstractTerm())
			if((_ABSTRACTTERM(To).getVar().getType())==getVar().getType()){
				   BoundedTermVariable NewVar(getVar().getType());
				   Token::pointer Left = To.applyArgument(NewVar);
				   Token::pointer Right = this->applyArgument(NewVar);
				   bool Res = (*Left==*Right);
				   delete Left;
				   delete Right;
				   return Res;

				}
	return false;
}


Token::pointer AbstractTerm::replaceAll(Token::const_reference To1, Token::const_reference To2) const{	

	if(this->operator ==(To1))
		return To2.clone();

	if((To1.isType())&&(To2.isType())){
		TokenPair* newPair = (this->VarBody).replaceAll(To1,To2);
		AbstractTerm* Res = new AbstractTerm(_TERM(newPair->getRight()),_TERM(newPair->getLeft()));
		delete newPair;
		return Res;
		}

	if((To1.isTerm())&&(To2.isTerm())){
		Token* NewBody = getBody().replaceAll(To1, To2);
		AbstractTerm* Res = new AbstractTerm(_TERM(*NewBody),getVar());
		delete NewBody;
		return Res;
		}

	throw Term::exception("Token::pointer AbstractTerm::replaceAll(Token::const_reference To1, Token::const_reference To2) const");
}

Term::pointer AbstractTerm::curry(Term::const_reference Ter){			
	if(Ter.getType().isArrowType()){
			FreeTermVariable x(_ARROWTYPE(Ter.getType()).getLeft());
			ApplicationTerm Body(Ter, x," ");
			return  new AbstractTerm(Body, x);
		}
throw Term::exception("Non arrowTyped argument to Term::pointer AbstractTerm::curry(Term::const_reference Ter)");	
}



AbstractTerm::AbstractTerm(Term::const_reference Te1, Term::const_reference Te2, const string& ss):
Term(ArrowType(Te2.getType(), Te1.getType()), ss),VarBody(Te1,Te1){
		BoundedTermVariable Var(Te2.getType());
		Token::pointer Body = Te1.replaceAll(Te2,Var);
		VarBody = TokenPair(Var, *Body);
		delete Body;
}

AbstractTerm::AbstractTerm(const AbstractTerm& Te):
Term(Te),VarBody(Te.VarBody){
}


AbstractTerm::~AbstractTerm()
{}

//#endif

// AbstractionTerm member functions
